System F
1972年
定義
code:bnf
項t = x
| λx:A.t
| Λα.t // genricな型
| t t // 関数適用
| tA // 型適用. []をつけずにtAと書くこともある 型A = α
| A1 -> A2
| ∀α.A
文脈Γ = <>
| <Γ,x:A>
補足
αは型変数
xは変数
Λは型レベルのラムダ抽象
つまりGenricな型のこと
型を引数に取り、型を返す
Λt.tというラムダ抽象を型t1に適用して、t1になる感じ
λは値レベルのラムダ抽象
λx:A.tは、括弧を付けるならλ(x:A).t
引数xがAで型付けされることで定義域が明示されている
「項t」は、「値レベルのラムダ抽象」と、「型レベルのラムダ抽象」の両方を表す
変数には値のみが代入でき、型変数には型のみが代入できる、という前提がある
t[A]は型Aを関数tに代入しているが、これは暗黙的にtはΛで表現される方のラムダ抽象である
この表記はTaPLに倣っている
一般的には角括弧は書かずにtAと書く
つまり小文字か大文字かで、関数適用か型適用かを判断する
例
恒等関数idをSystem Fで書く
id = Λa.λ(x:a).x
このときid: ∀α.α->α
まずなんらかの型を適用することで、その型に対する恒等関数にする
idBool = id Bool = λx:Bool.x
Bool型を適用することで、Bool型用のidにした
関連
参考
一番わかり易い